(declare-fun real_var242 () Real)
(declare-fun real_var1068 () Real)
(declare-fun real_var723 () Real)
(declare-fun real_var542 () Real)
(declare-fun real_var1201 () Real)
(declare-fun real_var1054 () Real)
(declare-fun real_var537 () Real)
(declare-fun real_var209 () Real)
(declare-fun real_var709 () Real)
(declare-fun real_var722 () Real)
(declare-fun real_var461 () Real)
(declare-fun real_var742 () Real)
(declare-fun real_var1276 () Real)
(declare-fun real_var1202 () Real)
(declare-fun real_var652 () Real)
(declare-fun real_var207 () Real)
(declare-fun real_var204 () Real)
(declare-fun real_var1065 () Real)
(declare-fun real_var1318 () Real)
(declare-fun real_var1275 () Real)
(declare-fun real_var1319 () Real)
(declare-fun real_var945 () Real)
(declare-fun real_var538 () Real)
(declare-fun real_var6 () Real)
(declare-fun real_var45 () Real)
(declare-fun real_var462 () Real)
(declare-fun real_var748 () Real)
(declare-fun real_var1200 () Real)
(declare-fun real_var539 () Real)
(declare-fun real_var92 () Real)
(declare-fun real_var862 () Real)
(declare-fun real_var427 () Real)
(declare-fun real_var141 () Real)
(declare-fun real_var1055 () Real)
(declare-fun real_var1066 () Real)
(declare-fun real_var59 () Real)
(declare-fun real_var459 () Real)
(declare-fun real_var1279 () Real)
(declare-fun real_var655 () Real)
(declare-fun real_var641 () Real)
(declare-fun real_var142 () Real)
(declare-fun real_var84 () Real)
(declare-fun real_var654 () Real)
(declare-fun real_var642 () Real)
(declare-fun real_var1073 () Real)
(declare-fun real_var653 () Real)
(declare-fun real_var46 () Real)
(declare-fun real_var140 () Real)
(declare-fun real_var99 () Real)
(declare-fun real_var428 () Real)
(declare-fun real_var205 () Real)
(declare-fun real_var186 () Real)
(declare-fun real_var746 () Real)
(declare-fun real_var1067 () Real)
(declare-fun real_var708 () Real)
(declare-fun real_var196 () Real)
(declare-fun real_var741 () Real)
(declare-fun real_var1277 () Real)
(declare-fun real_var208 () Real)
(declare-fun real_var747 () Real)
(declare-fun real_var1278 () Real)
(declare-fun real_var187 () Real)
(declare-fun real_var707 () Real)
(declare-fun real_var206 () Real)
(declare-fun real_var749 () Real)
(assert (or (and (not (exists ((REAL_VAR427 Real)) (=> (< 0.0 real_var242) (< (* real_var427 (/ 0 (* 2.0 (+ 6 real_var428)))) 0)))) (not (exists ((REAL_VAR641 Real)) (=> (and (=> (> 0.0 (* real_var1319 real_var1318)) (and (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (>= real_var862 0))) (= real_var140 (mod (to_int real_var141) (to_int real_var142)) (/ real_var141 real_var140)) (<= (+ (* real_var742 real_var741) (- real_var746 real_var747)) (- real_var748 real_var749)) (<= (/ (- 1) real_var538 real_var539 real_var537) real_var542) (< (/ 115 real_var206 real_var209) (/ 137 real_var207 real_var208)) (> 0.0 real_var6)) (= 0.0 (/ real_var641 (/ 423505801.1 real_var641)) 0.62829 real_var642))))) (not (exists ((REAL_VAR1065 Real)) (=> (and (=> (= real_var204 (+ real_var205 real_var196)) (= (+ (* real_var1201 real_var1200) (* (- 1) real_var1201 real_var1202) (* (- 1) real_var1200) (* (- 1) real_var1201 real_var1200 real_var1200) (* real_var1201 real_var1200 real_var1202)) (- 1))) (< 0.0 real_var1065 (/ real_var1066 (* (/ real_var1067 (/ 0.9 real_var1068)) real_var1065 7.0 real_var1065))) (< 0.0 3.0 (/ (+ 0.0 (/ 0.5277230151 0.0) (/ 325285732.0 real_var186)) real_var187) real_var186) (= real_var1073 (exp 0.4))) (< real_var459 real_var461 (/ 0.8545 real_var462)))))))
(assert (forall ((REAL_VAR1073 Real)) (or (and (= real_var1073 (exp 0.4)) (= real_var1054 0 real_var1055) (<= 0 real_var59)) (= (- real_var707 real_var708) real_var709))))
(check-sat)
